\chapter{协议的安全分析}
协议的分析方法有很多，针对不同的目标，有不同的形式化分析方法，我们这里主要介绍针对某个或某些安全目标的协议分析理论和方法。对于形式化分析方法，构造的形式化系统的描述能力和推理能力是很重要的两方面。
\section{BAN逻辑\cite{qing-cry}\footnotemark}
\footnotetext{本节内容摘录自卿斯汉老师“密码学与计算机网络安全”一书中的"11.1 认证协议和BAN逻辑".}
\subsection{基本概念}
BAN逻辑是一种基于信念的模态逻辑,是1989年由 Michael Burrows, Martin Ab
di和 Roger Needham提出的\footnote{论文公开发表于1990年，Michael Burrows, Martin Abadi, and Roger Needham. 1990. A logic of authentication. ACM Trans. Comput. Syst. 8, 1 (Feb. 1990), 18–36. DOI: \url{https://doi.org/10.1145/77648.77649}}.在BAN逻辑的推理过程中,参加协议的主体的信念随消
息交换的发展,不断变化和发展.应用BAN逻辑时,首先需进行“理想化步骤”,将协议的
消息转换为BAN逻辑中的公式,再根据具体情况进行合理的假设,由逻辑的推理规则根
据理想化协议和假设进行推理,推断协议能否完成预期的目标,依照BAN逻辑的惯例,
A,B,S通常表示具体的主体;$K_{ab},K_{as},K_{bs}$等表示具体的共享密钥;$K_a,K_b,K_c$等表示具
体的公开密钥;$K_a^{-1}1,K_b^{-1},K_c^1$等表示相应的秘密密钥;$N_a,N_a,N_c$等表示临时值;P,Q
和R表示任意主体;X和Y表示任意语句;K表示任意密钥.\par
BAN逻辑的结构如下,其中P,Q,R,X,Y,K等的含义如上所述.\par
\begin{table}[htbp]
		\centering 
		\caption{ BAN逻辑符号定义 } 
		\label{BAN-CHAR}
		\begin{tabular}{|c|c|}
			\hline 
			语义&符号表示  \\ 
			\hline 
			P believes X&P相信X  \\ 
			\hline 
			P sees X&P曾收到X  \\ 
			\hline 
			P said X&P曾发送X  \\ 
			\hline 
			P controls X&P对X有管辖权  \\ 
			\hline 
			(X,Y)&X和Y链接  \\ 
			\hline 
			fresh(X)&X是新的  \\ 
			\hline 
			${X}_K$&用K加密X后的结果  \\ 
			\hline 
			$P\stackrel{\kappa}{\leftrightarrow} Q$&P和Q可用共享密钥$\kappa$通信  \\ 
			\hline 
			H(X)&X是单向杂凑函数  \\ 
			\hline 
			$\stackrel{\kappa}{\rightarrow} P$&$\kappa$是P的公开密钥  \\ 
			\hline 
			$<X>_Y$&$<X,Y>\wedge Y$是某种秘密  \\ 
			\hline 
		\end{tabular} 
\end{table}
\par

\subsection{逻辑公设}
BAN逻辑的主要有以下5条逻辑公设：
\begin{enumerate}
	\item 消息含义法则逻辑公设\[\frac{P\ believes\ Q \stackrel{K}{\leftrightarrow}P,P\ sees\ {X}_K}{P\ believes\ Q\ said\ X}\]
	这一逻辑公设说明：如果P相信K是P和Q之间的共享密钥，且P曾收到用K加密X后的结果，则P相信Q曾发送过X。
	对于公钥系统，我们有类似的公设：\[\frac{P\  believes\  \stackrel{K}{\mapsto}\ Q,P\ sees\ {X}_{K^{-1}}}{P\ believes\ Q\ said\ X}\]
	
	\item 临时值校验法则逻辑公设\[\frac{P\ believes\ fresh(X) ,P\ believes\ Q\ said\ X}{P\ believes\ Q\ believes\ X}\]
	这一逻辑公设说明：如果P相信消息X是新的，且P相信Q曾发送过X，则P相信Q相信X。
	
	\item 管辖法则逻辑公设\[\frac{P\ believes\ Q\ controls\ X ,P\ believes\ Q\ believes\ X}{P\ believes\ X}\]
	这一逻辑公设说明：如果P相信Q对X具有管辖权，且P相信Q相信X，则P相信X。
	
	\item 逻辑公设
	\[
	\frac{P\ sees\ (X,Y)}{P sees X}\qquad \frac{P\ sees <X>_Y}{P sees X}
	\]
	\[
	\frac{P\ believes\ Q\stackrel{K}{\leftrightarrow}P ,P\ sees\ {X}_K}{P\ sees\ X}
	\]
	\[
	\frac{P\  believes\  \stackrel{K}{\mapsto}\ P,P\ sees\ {X}_{K}}{P\ sees\ X}
	\]
	\[
	\frac{P\  believes\  \stackrel{K}{\mapsto}\ Q,P\ sees\ {X}_{K^{-1}}}{P\ sees\ X}
	\]
	这一逻辑公设说明：如果一个主体曾收到一个公式，且该主体知道相关的密钥，则该主体曾收到该公式的组成部分。
	
	\item 逻辑公设\[\frac{P\ believes fresh(X)}{P\ believes\ fresh\ (X,Y)}\]
	这一逻辑公设说明：如果一个公式的一部分是新的，则该公式全部是新的。
\end{enumerate}

\subsection{推理步骤}
BAN逻辑的推理步骤是:\par
(1)建立初始假设集合$\alpha$;\par
(2)建立理想化协议模型;\par
(3)建立协议预期目标集合$\gamma$;\par
(4)利用初设和逻辑公设推理;\par
(5)推导出协议最终目标集合$\varGamma$;\par
(6)若$\varGamma \supseteq \gamma $,则协议可行.\par
以上步骤可能会重复进行,例如:通过分析增加新的初设、改进理想化协议等.通过
BAN逻辑分析,可以回答下述问题:认证协议是否正确\footnote{何为正确？},认证协议的目标是否达到,认证
协议的初设是否合适,认证协议是否冗余.\par

\subsection{分析Needham-Schroeder协议}

\subsubsection{初始假设集合}
$A\ believes\ A \stackrel{K_{as}}{\leftrightarrow}S$ \hspace{2cm} $B\ believes\ B \stackrel{K_{bs}}{\leftrightarrow}S$
\par
$S\ believes\ A \stackrel{K_{as}}{\leftrightarrow}S$ \hspace{2cm} $S\ believes\ B \stackrel{K_{bs}}{\leftrightarrow}S$
\par
$S\ believes\ A \stackrel{K_{ab}}{\leftrightarrow}B$
\par
$A\ believes\ S\ controls\ A \stackrel{K}{\leftrightarrow}B$ \hspace{2cm} $B\ believes\ S\ controls\ A \stackrel{K}{\leftrightarrow}B$
\par
$A\ believes\ S\ controls\ fresh\ (A\stackrel{K}{\leftrightarrow}B)$ 
\par
$A\ believes\ fresh\ (N_a)$ \hspace{2cm} $B\ believes\ fresh\ (N_b)$
\par
$S\ believes\ fresh\ (A \stackrel{K}{\leftrightarrow}B)$ \hspace{2cm} $B\ believes\ fresh\ (A \stackrel{K}{\leftrightarrow}B)$
\par
以上大部分初始假设都是自然的，第一组5个初始假设涉及主体拥有的初始密钥。下面3个初始假设说明客户相信认证服务器所具有的功能。如同上例，A和B相信认证服务器S能为A和B生成新的会话密钥。但是，在此处A还相信S所生成的会话密钥同时具有临时值的性质。以上初始假设是有道理的，因为一个“好”的加密密钥通常具备临时值的特征。最后4个初始假设指出，相关的临时值是新的。\par

下面要特别讨论的是最后一个初始假设
\[B\ believes\ fresh\ (A \stackrel{K}{\leftrightarrow}B)\]
这个假设是不寻常的。在下面的讨论中，我们将说明，许多对此协议的批评均来自这个假设，而协议的发明者并未认识到他们实际上应用了这一假设。

\subsubsection{理想化协议模型}
去掉与协议分析无关部分，理想化协议模型为：
\begin{enumerate}
	\item $S\rightarrow A\ :\  \left\lbrace N_a,(A\stackrel{K_{ab}}{\leftrightarrow}B),\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B),(A\stackrel{K_{ab}})_{K_{bs}} \right\rbrace_{K_{as}} $
	\item $A\rightarrow B\ :\ (A\stackrel{K_{ab}}{\leftrightarrow}B)_{K_{bs}} $
	\item $B\rightarrow A\ :\  \left\lbrace N_b, A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace_{K_{ab}}$ from B
	\item $A\rightarrow B\ :\  \left\lbrace N_b, A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace _{K_{ab}}$ from A
\end{enumerate}
在3，4条中包含了发送者的名称，为的是区分两条消息，避免混淆。在原协议中，区分的方法是通过$N_b$
和$N_b -1 $实现的，事实上，在原协议中$N_b -1 $可以用任何$N_b$的函数来取代。\par
在理想化协议模型中，1，3，4条消息中关于$K_{ab}$的语句说明，A可以将会话密钥$K_{ab}$作为临时值应用，同时每个客户均认可对方相信该会话密钥$K_{ab}$是“好”密钥。


\subsubsection{建立协议预期目标}
协议的预期目标是：
\[A\ believes\ A \stackrel{K_{ab}}{\leftrightarrow} B \]
\[B\ believes\ A \stackrel{K_{ab}}{\leftrightarrow} B \]

\subsubsection{利用初设和逻辑公设推理}
$\bullet$ \textbf{消息$S\rightarrow A\ :\  \left\lbrace N_a,(A\stackrel{K_{ab}}{\leftrightarrow}B),\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B),(A\stackrel{K_{ab}})_{K_{bs}} \right\rbrace_{K_{as}} $的推导链条}\par

由消息$S\rightarrow A\ :\  \left\lbrace N_a,(A\stackrel{K_{ab}}{\leftrightarrow}B),\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B),(A\stackrel{K_{ab}})_{K_{bs}} \right\rbrace_{K_{as}} $，我们可知:\\

$A\ sees\ \left\lbrace N_a,(A\stackrel{K_{ab}}{\leftrightarrow}B),\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B),(A\stackrel{K_{ab}})_{K_{bs}} \right\rbrace_{K_{as}} $\\

$\xLongrightarrow{A\ believes\ A\stackrel{K_{as}}{\leftrightarrow}S;\frac{P\ believes\ Q \stackrel{K}{\leftrightarrow}P,P\ sees\ {X}_K}{P\ believes\ Q\ said\ X}}$\\

$A\ belives\ S\ said\ (N_a,A\stackrel{K_{ab}}{\leftrightarrow}B,fresh(A\stackrel{K_{ab}}{\leftrightarrow}B))$\\

$\xLongrightarrow{A\ believes\ fresh(N_a);\frac{P\ believes\ fresh(X) ,P\ believes\ Q\ said\ X}{P\ believes\ Q\ believes\ X}}$\\

$
\begin{cases}
	A\ believers\ S\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result1} \\
	A\ believers\ S\ believes\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result2})
\end{cases}
$
\\

$\xLongrightarrow[\frac{P\ believes\ Q\ controls\ X ,P\ believes\ Q\ believes\ X}{P\ believes\ X}]{
A\ believes\ S\ controls\ A \stackrel{K}{\leftrightarrow}B;A\ believes\ S\ controls\ fresh\ (A\stackrel{K}{\leftrightarrow}B)
}$\\

$
\begin{cases}
A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result3} \\
A\ believes\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result4})
\end{cases}
$
\\
\par

另外：\\

$A\ sees\ \left\lbrace N_a,(A\stackrel{K_{ab}}{\leftrightarrow}B),\ fresh(A\stackrel{K_{ab}}{\leftrightarrow}B),(A\stackrel{K_{ab}})_{K_{bs}} \right\rbrace_{K_{as}} $\\

$\xLongrightarrow{\text{消息中包含要推出内容}}$\\

$A\ sees\ \{ A\stackrel{K_{ab}}{\leftrightarrow}B \} \ldots \ldots \text{记为Result5}$
\par

\vspace{1cm}

$\bullet$ \textbf{消息$A\rightarrow B\ :\ (A\stackrel{K_{ab}}{\leftrightarrow}B)_{K_{bs}} $的推导链条}\par

由消息$A\rightarrow B\ :\ (A\stackrel{K_{ab}}{\leftrightarrow}B)_{K_{bs}} $，我们可知：\\

$B\ sees\ (A\stackrel{K_{ab}}{\leftrightarrow}B)_{K_{bs}}$\\
	
$\xLongrightarrow{B\ believes\ B\stackrel{K_{bs}}{\leftrightarrow}S;\frac{P\ believes\ Q \stackrel{K}{\leftrightarrow}P,P\ sees\ {X}_K}{P\ believes\ Q\ said\ X}}$\\

$B\ believers\ S\ said\ A\stackrel{K_{ab}}{\leftrightarrow}B$\\

因为B只能假定来自认证服务器S的消息是新的，而不能断定A发送的消息是新的还是重放的消息，所以，我们无法继续分析和证明下去，除非加上那条可疑的初始假设：
\[B\ believes\ fresh\ (A \stackrel{K}{\leftrightarrow}B)\]
\par

一旦利用这个初始假设，我们可以继续推导。\par

$B\ believers\ S\ said\ A\stackrel{K_{ab}}{\leftrightarrow}B$\\

$\xLongrightarrow{B\ believes\ fresh\ (A \stackrel{K}{\leftrightarrow}B);\frac{P\ believes\ fresh(X) ,P\ believes\ Q\ said\ X}{P\ believes\ Q\ believes\ X}}$\\

$B\ believes\ S\ believes\ A \stackrel{K}{\leftrightarrow}B \ldots \ldots \text{记为Result6}$\\

$B\ believers\ S\ said\ A\stackrel{K_{ab}}{\leftrightarrow}B$\\

$\xLongrightarrow{B\ believes\ S\ controls\ A \stackrel{K}{\leftrightarrow}B;\frac{P\ believes\ Q\ controls\ X ,P\ believes\ Q\ believes\ X}{P\ believes\ X}}$\\

$B\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result7}$\\


我们根据Result3:$A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B$和消息“$B\rightarrow A\ :\  \left\lbrace N_b, A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace_{K_{ab}}$ from B”可以进行如下推理：\\

$B\rightarrow A\ :\  \left\lbrace N_b, A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace_{K_{ab}}$\\

$\xLongrightarrow{A\text{收到消息}}$\\

$A\ sees\ \left\lbrace A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace_{K_{ab}}$\\

$\xLongrightarrow{A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B;\frac{P\ believes\ Q \stackrel{K}{\leftrightarrow}P,P\ sees\ {X}_K}{P\ believes\ Q\ said\ X}}$\\

$A\ believes\ B\ said\ A\stackrel{K_{ab}}{\leftrightarrow}B$\\

$\xLongrightarrow{Result4;\frac{P\ believes\ fresh(X) ,P\ believes\ Q\ said\ X}{P\ believes\ Q\ believes\ X}}$

$A\ believes\ B\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result8}$
\par

类似，我们根据消息:"$A\rightarrow B\ :\  \left\lbrace N_b, A\stackrel{K_{ab}}{\leftrightarrow}B\right\rbrace _{K_{ab}}$ from A"可以推出:
\[B\ believes\ A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result9}\]

\subsubsection{推导出协议最终目标集合}
至此为止，我们推导出的最终目标集合有Result3、Result7、Result8、Result9，即：\\
$
\begin{cases}
A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result3} \\
B\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result7}\\
A\ believes\ B\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result8}\\
B\ believes\ A\ believes\ A\stackrel{K_{ab}}{\leftrightarrow}B \ldots \ldots \text{记为Result9}
\end{cases}
$
\par
将最终目标集合和预期目标集合比较，可知预期目标集合是最终目标集合的子集，也就是说协议达到预期目的。


\subsubsection{讨论}
Needham-Schroeder协议得出了较强的结论，其代价是：必须额外假定B获得的会话密钥时新的会话密钥。这一代价是巨大的，一次招致许多批评，也为Needham--Schroeder协议的进一步改进提供了依据。主要原因是：一旦会话密钥被破译会带来严重的后果。攻击者可以有无限的时间去寻找一个旧的会话密钥，然后重新使用它，好像这个密钥时新的密钥。很明显，问题出在B和认证服务器S没有打交道。这样，上述BAN逻辑的形式化分析过程就为Needham--Schroeder协议的改进提供了方向。例如，一种改进方法是：认证服务器S先发送消息给B而不是A，这里就不在赘述了。\par

另外，从BAN逻辑的形式化分析过程我们也看到一些Needham-Schroeder协议的冗余性。例如，在第2条消息中，认证证书$\{K_{ab},A\}_{K_b}$通过A的密钥$K_{as}$加密是没有必要的。因为，这个认证证书随后立即由A发送给B，没有再继续加密。从BAN逻辑形式化分析的整个过程来看，这种加密丝毫不影响分析和证明的过程，旁证了认证证书$\{K_{ab},A\}_{K_b}$通过A的密钥$K_{as}$加密的冗余性。\par

这个例子证明了BAN逻辑在分析认证协议时的重要作用，它可以证明协议的正确性和安全性，发现协议中不易察觉的缺陷，指出进一步改进认证协议的方向。


\section{逻辑编程和协议分析工具}
除了使用一些针对安全协议分析设计的逻辑工具外，有一些通用的逻辑编程语言，如Prolog、Datalog可以用于协议分析，还有一些形式化语言，比如Z语言，也可以用于协议安全分析。